<html><body>Utility classes used by jEdit but that do not depend on jEdit
itself.</body></html>
